Nuprl Lemma : es-locl-iff 11,40

the_es:event_system{i:l}, e,e':es-E(the_es).
es-locl(the_esee')
 (((es-first(the_ese')))
  ((e = es-pred(the_ese'))  es-locl(the_ese; es-pred(the_ese')))) 
latex


Definitionsx:AB(x), t  T, P  Q, P  Q, P  Q, P  Q, A c B, P  Q, prop{i:l}, A, guard(T), False, trans(Tx,y.E(x;y))
Lemmases-axioms, event system wf, es-locl wf, not wf, assert wf, es-first wf, es-E wf, es-pred wf, Id wf, es-loc wf, es-loc-pred

origin